Nuprl Definition : ma-send
11,40
postcript
pdf
M
.send(
k
;
l
;
s
;
v
;
ms
;
i
)
==
L
!= (
M
.2.2.2.2.2).1(<
k
,
l
>)
==
==
ms
= if source(
l
) =
i
then concat(map(
tgf
.map(
x
.<
tgf
.1,
x
>;(
tgf
.2)(
s
,
v
));
L
)) else [] fi
latex
clarification:
M
.send(
k
;
l
;
s
;
v
;
ms
;
i
)
== fpf-val(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);
== fpf-val(
((
M
.2.2.2.2.2).1);
== fpf-val(
<
k
,
l
>;
== fpf-val(
k
,
L
.(
ms
== fpf-val(
k
,
L
.(
=
== fpf-val(
k
,
L
.(
if source(
l
) =
i
== fpf-val(
k
,
L
.(
then concat(map(
tgf
.map(
x
.<
tgf
.1,
x
>;(
tgf
.2)(
s
,
v
));
L
))
== fpf-val(
k
,
L
.(
else []
== fpf-val(
k
,
L
.(
fi
== fpf-val(
k
,
L
.(
((
tg
:Id
if source(
l
) =
i
then
M
.da(rcv(
l
,
tg
)) else Top fi ) List)))
latex
Definitions
z
!=
f
(
x
)
P
(
a
;
z
)
,
product-deq(
A
;
B
;
a
;
b
)
,
Knd
,
IdLnk
,
KindDeq
,
IdLnkDeq
,
s
=
t
,
type
List
,
x
:
A
B
(
x
)
,
Id
,
M
.da(
a
)
,
rcv(
l
,
tg
)
,
Top
,
if
b
then
t
else
f
fi
,
a
=
b
,
source(
l
)
,
concat(
ll
)
,
map(
f
;
as
)
,
x
.
A
(
x
)
,
<
a
,
b
>
,
t
.1
,
f
(
a
)
,
t
.2
,
[]
FDL editor aliases
ma-send
origin